2021
Other
Unknown
Sito Web "Pubblicare Open Access al CNR"
Giannini S., Trentanni G., Maggi R., Mangiaracina S.
Il portale si propone come strumento di comunicazione e luogo di raccolta delle informazioni necessarie agli autori CNR per pubblicare in accesso aperto in modo consapevole. Negli ultimi due anni le pubblicazioni in accesso aperto degli autori CNR sono cresciute molto. Navigando all'interno delle sezioni del sito è possibile acquisire indicazioni sulle modalità di pubblicazione in accesso aperto; sui contratti Read&Publish stipulati con gli editori; sulle agevolazioni previste per la pubblicazione in accesso aperto e sugli strumenti utilizzabili per "fare concretamente Open Access".
Giannini S., Trentanni G., Maggi R., Mangiaracina S.
Il portale si propone come strumento di comunicazione e luogo di raccolta delle informazioni necessarie agli autori CNR per pubblicare in accesso aperto in modo consapevole. Negli ultimi due anni le pubblicazioni in accesso aperto degli autori CNR sono cresciute molto. Navigando all'interno delle sezioni del sito è possibile acquisire indicazioni sulle modalità di pubblicazione in accesso aperto; sui contratti Read&Publish stipulati con gli editori; sulle agevolazioni previste per la pubblicazione in accesso aperto e sugli strumenti utilizzabili per "fare concretamente Open Access".
See at: openaccess.cnr.it | CNR ExploRA
2021
Other
Unknown
Sito web del laboratorio ISTI "Formal Methods & Tools"
Trentanni G.
Web Site related to the Formal Methods and Tools (FMT) Laboratory afferent to the Institute of Information Science and Technologies "Alessandro Faedo" (ISTI) of the National Research Council of Italy (CNR)
Trentanni G.
Web Site related to the Formal Methods and Tools (FMT) Laboratory afferent to the Institute of Information Science and Technologies "Alessandro Faedo" (ISTI) of the National Research Council of Italy (CNR)
See at: CNR ExploRA | www.fmt.isti.cnr.it
2020
Other
Unknown
Sito web GL2020 - 22nd International Conference on Grey Literature "Applications of Grey Literature for Science and Society"
Trentanni G., Giannini S., Molino A.
Sito web della conferenza internazionale sulla letteratura grigia GL2020: 22nd International Conference on Grey Literature "Applications of Grey Literature for Science and Society".
Trentanni G., Giannini S., Molino A.
Sito web della conferenza internazionale sulla letteratura grigia GL2020: 22nd International Conference on Grey Literature "Applications of Grey Literature for Science and Society".
See at: gl2020.isti.cnr.it | CNR ExploRA
2019
Contribution to book
Closed Access
Comparing results of natural language disambiguation tools with reports of manual reviews of safety-related standards
Biscoglio I., Ciancabilla A., Fusani M., Lami G., Trentanni G.
Methods and tools for detecting and measuring ambiguity in texts have been proposed for years, yet their efficacy is still under study for improvement, encouraged by results in various application fields (requirements, legal documents, interviews, ...). The paper presents a fresh-started process aimed at validating such methods and tools by applying some of them to a semi-structured data corpus. This corpus represents results of manual reviews, done by international experts, along with their source texts. The purpose is to check how much results of automated analysis are consistent with the reviewers reports. The application domain is that of safety-related system/software Standards in Railway. Thus, if we increase confidence in tools, then we also increase confidence in Standard correctness, which in turn impacts in conforming products.Source: From Software Engineering to Formal Methods and Tools, and Back, edited by Maurice H. ter Beek, Alessandro Fantechi, Laura Semini, pp. 239–249. Cham, Heidelberg, New York, Dordrecht, London: Springer, 2019
DOI: 10.1007/978-3-030-30985-5_15
Metrics:
Biscoglio I., Ciancabilla A., Fusani M., Lami G., Trentanni G.
Methods and tools for detecting and measuring ambiguity in texts have been proposed for years, yet their efficacy is still under study for improvement, encouraged by results in various application fields (requirements, legal documents, interviews, ...). The paper presents a fresh-started process aimed at validating such methods and tools by applying some of them to a semi-structured data corpus. This corpus represents results of manual reviews, done by international experts, along with their source texts. The purpose is to check how much results of automated analysis are consistent with the reviewers reports. The application domain is that of safety-related system/software Standards in Railway. Thus, if we increase confidence in tools, then we also increase confidence in Standard correctness, which in turn impacts in conforming products.Source: From Software Engineering to Formal Methods and Tools, and Back, edited by Maurice H. ter Beek, Alessandro Fantechi, Laura Semini, pp. 239–249. Cham, Heidelberg, New York, Dordrecht, London: Springer, 2019
DOI: 10.1007/978-3-030-30985-5_15
Metrics:
See at:
doi.org 
| link.springer.com | CNR ExploRA
2019
Contribution to book
Closed Access
QuARS: a pioneer tool for NL requirement analysis
Lami G., Fusani M., Trentanni G.
This paper summarizes the achievements of Stefania Gnesi's research activity in the area of the natural language requirements analysis and quality evaluation. The development of the QuARS tool has been the pivotal step of this research stream led by Stefania Gnesi at ISTI-CNR. A functional description of the QuARS tool is provided as well as a short report of its evolutions over a decade. The wide use of QuARS in several research and industrial contexts demonstrates the validity and the originality of Stefania's contribution in such an area of software engineering.Source: From Software Engineering to Formal Methods and Tools, and Back, edited by ter Beek M.H.; Fantechi A.; Semini L., pp. 211–219. Cham, Heidelberg, New York, Dordrecht, London: Springer, 2019
DOI: 10.1007/978-3-030-30985-5_13
Metrics:
Lami G., Fusani M., Trentanni G.
This paper summarizes the achievements of Stefania Gnesi's research activity in the area of the natural language requirements analysis and quality evaluation. The development of the QuARS tool has been the pivotal step of this research stream led by Stefania Gnesi at ISTI-CNR. A functional description of the QuARS tool is provided as well as a short report of its evolutions over a decade. The wide use of QuARS in several research and industrial contexts demonstrates the validity and the originality of Stefania's contribution in such an area of software engineering.Source: From Software Engineering to Formal Methods and Tools, and Back, edited by ter Beek M.H.; Fantechi A.; Semini L., pp. 211–219. Cham, Heidelberg, New York, Dordrecht, London: Springer, 2019
DOI: 10.1007/978-3-030-30985-5_13
Metrics:
See at:
doi.org | link.springer.com | CNR ExploRA
2019
Conference article
Open Access
QuARS: a NLP tool for requirements analysis
Gnesi S., Trentanni G.
QuARS (Quality Analyzer for Requirements Specifications) is a tool able to perform an analysis of Natural Language (NL) requirements in a systematic and an automatic way by means of natural language processing techniques with a focus on ambiguity detection. QuARS allows the requirements engineers to perform an early analysis of the requirements for automatically detecting potential linguistic defects.Source: REFSQ-2019 - Workshops, Doctoral Symposium, Live Studies Track, and Poster Track, Essen, Germany, 19 March, 2019
Gnesi S., Trentanni G.
QuARS (Quality Analyzer for Requirements Specifications) is a tool able to perform an analysis of Natural Language (NL) requirements in a systematic and an automatic way by means of natural language processing techniques with a focus on ambiguity detection. QuARS allows the requirements engineers to perform an early analysis of the requirements for automatically detecting potential linguistic defects.Source: REFSQ-2019 - Workshops, Doctoral Symposium, Live Studies Track, and Poster Track, Essen, Germany, 19 March, 2019
See at:
ceur-ws.org 
| ISTI Repository | CNR ExploRA
2018
Other
Unknown
Sito web Biblioteca Area CNR Pisa
Volpini F., Giannini S., Molino A., D'Angelo C., Lombardi S., Trentanni G.
Lo sviluppo del nuovo sito web nasce principalmente dall'esigenza di rimanere al passo con i tempi, sia dal punto di vista del restyling grafico, sia dalla necessità di fornire contenuti adeguati ai nuovi scenari in cui si muove la ricerca scientifica e ai cambiamenti in atto nelle modalità di comunicazione dei risultati della ricerca stessa. Non ultima motivazione è costituita dalla possibilità fornita dalle nuove tecnologie web che consentono di rendere maggiormente fruibile il sito anche da dispositivi mobili quali tablet e smartphone. Il sito è stato progettato e sviluppato sfruttando il CMS Joomla. Di seguito sono elencati i contributi forniti dai singoli autori per la realizzazione del progetto. - Alla fase di progettazione hanno partecipato Federico Volpini, Silvia Giannini, Anna Molino, Caterina D'Angelo e Gianluca Trentanni. - Caterina D'Angelo ha predisposto il server web sul quale Federico Volpini ha installato il CMS Joomla, ha collaborato all'organizzazione di alcuni contenuti e mantiene il server con il ruolo di amministratore. - Federico Volpini ha curato lo sviluppo del sito, in particolare del template e del modulo per la ricerca dei libri di testo. - I contenuti sono stati prodotti da Silvia Giannini e Anna Molino. Silvia Giannini ha curato i contenuti e l'inserimento degli stessi in italiano mentre Anna Molino ha curato la traduzione e l'inserimento in lingua inglese. - Stefania Lombardi ha curato i contenuti e la pubblicazione della sezione News. - Daniela Falconetti ha realizzato tutte le foto presenti nel banner, di cui è proprietaria. - Gianluca Trentanni ha curato la rielaborazione delle foto allo scopo di adattarle alla visualizzazione e, in alcunii casi, di ottenere effetti particolari.
Volpini F., Giannini S., Molino A., D'Angelo C., Lombardi S., Trentanni G.
Lo sviluppo del nuovo sito web nasce principalmente dall'esigenza di rimanere al passo con i tempi, sia dal punto di vista del restyling grafico, sia dalla necessità di fornire contenuti adeguati ai nuovi scenari in cui si muove la ricerca scientifica e ai cambiamenti in atto nelle modalità di comunicazione dei risultati della ricerca stessa. Non ultima motivazione è costituita dalla possibilità fornita dalle nuove tecnologie web che consentono di rendere maggiormente fruibile il sito anche da dispositivi mobili quali tablet e smartphone. Il sito è stato progettato e sviluppato sfruttando il CMS Joomla. Di seguito sono elencati i contributi forniti dai singoli autori per la realizzazione del progetto. - Alla fase di progettazione hanno partecipato Federico Volpini, Silvia Giannini, Anna Molino, Caterina D'Angelo e Gianluca Trentanni. - Caterina D'Angelo ha predisposto il server web sul quale Federico Volpini ha installato il CMS Joomla, ha collaborato all'organizzazione di alcuni contenuti e mantiene il server con il ruolo di amministratore. - Federico Volpini ha curato lo sviluppo del sito, in particolare del template e del modulo per la ricerca dei libri di testo. - I contenuti sono stati prodotti da Silvia Giannini e Anna Molino. Silvia Giannini ha curato i contenuti e l'inserimento degli stessi in italiano mentre Anna Molino ha curato la traduzione e l'inserimento in lingua inglese. - Stefania Lombardi ha curato i contenuti e la pubblicazione della sezione News. - Daniela Falconetti ha realizzato tutte le foto presenti nel banner, di cui è proprietaria. - Gianluca Trentanni ha curato la rielaborazione delle foto allo scopo di adattarle alla visualizzazione e, in alcunii casi, di ottenere effetti particolari.
See at: library.area.pi.cnr.it | CNR ExploRA
2018
Other
Unknown
Sito Web "BIBV - BIBliography of historic activity of Italian Volcanoes"
Giannini S., Trentanni G., Principe C., Paolillo A.
Il portale espone i contenuti della versione V della "Bibliografia storica dei vulcani attivi italiani" - BIBV V. Il portale offre possibilità di ricerca esclusive e funzionali, volte a migliorare l'esperienza dell'utente e aumentare l'efficienza e la velocità della ricerca.
Giannini S., Trentanni G., Principe C., Paolillo A.
Il portale espone i contenuti della versione V della "Bibliografia storica dei vulcani attivi italiani" - BIBV V. Il portale offre possibilità di ricerca esclusive e funzionali, volte a migliorare l'esperienza dell'utente e aumentare l'efficienza e la velocità della ricerca.
See at: libero.area.pi.cnr.it | CNR ExploRA
2017
Contribution to book
Restricted
Certification of cash registers software
Biscoglio I., Lami G., Trentanni G.
This paper presents the Italian scenario of cash register software certification. The basic concepts of certification are introduced together with involved actors, requirements and possible objects to be certified. Subsequently, the specific kind of fiscal device running fiscal software, that is the cash register, is outlined, and its certification process is described. The current technological adjustments of the cash register software according to the Italian legislation modifications are introduced and discussed.Source: Model-Driven Engineering and Software Development, edited by Slimane Hammoudi, Luís Ferreira Pires, Bran Selic, Philippe Desfray, pp. 154–167, 2017
DOI: 10.1007/978-3-319-66302-9_8
Metrics:
Biscoglio I., Lami G., Trentanni G.
This paper presents the Italian scenario of cash register software certification. The basic concepts of certification are introduced together with involved actors, requirements and possible objects to be certified. Subsequently, the specific kind of fiscal device running fiscal software, that is the cash register, is outlined, and its certification process is described. The current technological adjustments of the cash register software according to the Italian legislation modifications are introduced and discussed.Source: Model-Driven Engineering and Software Development, edited by Slimane Hammoudi, Luís Ferreira Pires, Bran Selic, Philippe Desfray, pp. 154–167, 2017
DOI: 10.1007/978-3-319-66302-9_8
Metrics:
See at:
doi.org | link.springer.com | CNR ExploRA
2016
Conference article
Unknown
Fiscal software certification: An Italian experience of certification against the fiscal legislation
Biscoglio I., Lami G., Trentanni G.
This paper describes an experience of software certification in the specific fiscal software domain. The Italian Fiscal Software Certification scenario and the cash register, as specific kind of fiscal device running fiscal software, are outlined. Besides, some requirements, extracted from the current legislation, are shown. As the Italian legislation does not provide it, a Business Process Model (BPM) presenting the fiscal software certification process is illustrated. The BPM was built by means of a study of the current legislation and it constitutes the original contribution to the paper. Finally, the challenges of the further technological adjustments according to the Italian legislation are discussed.Source: International Workshop on DomAin Specific Model-Based AppRoaches to vErificaTion and validaTiOn, pp. 54–61, Rome, Italy, 19 February 2016
Biscoglio I., Lami G., Trentanni G.
This paper describes an experience of software certification in the specific fiscal software domain. The Italian Fiscal Software Certification scenario and the cash register, as specific kind of fiscal device running fiscal software, are outlined. Besides, some requirements, extracted from the current legislation, are shown. As the Italian legislation does not provide it, a Business Process Model (BPM) presenting the fiscal software certification process is illustrated. The BPM was built by means of a study of the current legislation and it constitutes the original contribution to the paper. Finally, the challenges of the further technological adjustments according to the Italian legislation are discussed.Source: International Workshop on DomAin Specific Model-Based AppRoaches to vErificaTion and validaTiOn, pp. 54–61, Rome, Italy, 19 February 2016
See at: CNR ExploRA
2016
Report
Unknown
Certificazione del software fiscale. Un'esperienza italiana di certificazione conforme alla legislazione fiscale.
Biscoglio I., Trentanni G.
This paper presents the Italian scenario of cash register software certification. The basic concepts of certification are introduced together with involved actors, requirements and possible objects to be certified. Subsequently, the specific kind of fiscal device running fiscal software, that is the cash register, is outlined, and its certification process is described. The current technological adjustments of the cash register software according to the Italian legislation modifications are introduced and discussed.Source: ISTI Technical reports, 2016
Biscoglio I., Trentanni G.
This paper presents the Italian scenario of cash register software certification. The basic concepts of certification are introduced together with involved actors, requirements and possible objects to be certified. Subsequently, the specific kind of fiscal device running fiscal software, that is the cash register, is outlined, and its certification process is described. The current technological adjustments of the cash register software according to the Italian legislation modifications are introduced and discussed.Source: ISTI Technical reports, 2016
See at: CNR ExploRA
2015
Conference article
Restricted
Certification and legislation. An Italian experience of fiscal software certification
Biscoglio I., Lami G., Marchetti E., Trentanni G.
The paper introduces the Italian Fiscal Software Certification scenario. Some concepts about certification are illustrated. The cash registers, as specific kind of Fiscal Meter, are described and their adopted certification process based on Italian legislation requirements is presented as well. Finally, the new related technological challenges are discussed.Source: ICSOFT - EA 2015 - 10th International Conference on Software Engineering and Applications, pp. 174–179, Colmar, Alsace, France, 20 - 22 July 2015
Biscoglio I., Lami G., Marchetti E., Trentanni G.
The paper introduces the Italian Fiscal Software Certification scenario. Some concepts about certification are illustrated. The cash registers, as specific kind of Fiscal Meter, are described and their adopted certification process based on Italian legislation requirements is presented as well. Finally, the new related technological challenges are discussed.Source: ICSOFT - EA 2015 - 10th International Conference on Software Engineering and Applications, pp. 174–179, Colmar, Alsace, France, 20 - 22 July 2015
See at:
www.scitepress.org | CNR ExploRA
2014
Other
Unknown
Sito Web "SPLC 2014 - 18th International Software Product Line Conference"
Trentanni G.
Web Site related to the 18th International Software Product Line Conference (SPLC 2014)
Trentanni G.
Web Site related to the 18th International Software Product Line Conference (SPLC 2014)
See at: CNR ExploRA | splc2014.isti.cnr.it
2013
Contribution to book
Restricted
An application of stochastic model checking in the industry: user-centered modeling and analysis of collaboration in thinkteam
Ter Beek M. H., Gnesi S., Latella D., Massink M., Sebastianis M., Trentanni G.
In this chapter, we describe a general methodology for modeling and analyzing industrial software systems in their design phase, that is, prior to their implementation, by means of (stochastic) model checking.Source: Formal Methods for Industrial Critical Systems: A Survey of Applications, edited by Stefania Gnesi, Tiziana Margaria, pp. 179–203, 2013
DOI: 10.1002/9781118459898.ch9
Metrics:
Ter Beek M. H., Gnesi S., Latella D., Massink M., Sebastianis M., Trentanni G.
In this chapter, we describe a general methodology for modeling and analyzing industrial software systems in their design phase, that is, prior to their implementation, by means of (stochastic) model checking.Source: Formal Methods for Industrial Critical Systems: A Survey of Applications, edited by Stefania Gnesi, Tiziana Margaria, pp. 179–203, 2013
DOI: 10.1002/9781118459898.ch9
Metrics:
See at:
doi.org | onlinelibrary.wiley.com | CNR ExploRA
2013
Other
Unknown
Sito Web "Vamos 2013 - Seventh International Workshop on Variability Modelling of Software-intensive Systems"
Trentanni G.
Web Site related to the Seventh International Workshop on Variability Modelling of Software-intensive Systems (VAMOS) in 2013
Trentanni G.
Web Site related to the Seventh International Workshop on Variability Modelling of Software-intensive Systems (VAMOS) in 2013
See at: CNR ExploRA | vamos2013.isti.cnr.it
2012
Contribution to conference
Unknown
iFM 2012 & ABZ 2012 - Proceedings of the Posters & Tool demos Session
Mazzanti F., Trentanni G.
Submissions accepted for the Posters & Tool Demos Session at iFM+ABZ 2012 Conference, Pisa, 18-21 June 2012Source: Pisa: CNR-ISTI, 2012
Project(s): DEPLOY
Mazzanti F., Trentanni G.
Submissions accepted for the Posters & Tool Demos Session at iFM+ABZ 2012 Conference, Pisa, 18-21 June 2012Source: Pisa: CNR-ISTI, 2012
Project(s): DEPLOY
See at: CNR ExploRA
2012
Conference article
Restricted
A case study of requirements quality analysis
Biscoglio I., Coco A., Fabbrini F., Fusani M., Lami G., Marchetti E., Trentanni G.
Requirements analysis occupies a prominent part in the activities of a product life cycle. Out of the various aspects of the analysis, those related to the quality of requirements can have a large impact in the quality of the final product. Since requirements are first conceived as natural language expressions, and intensive use of automation is advised to keep project cost at reasonable level, it seems opportune to develop requirements analysis by means of natural language processing techniques. In spite of the scarce interest drawn by these issues within the industrial environment, the advantages of adopting natural language processing techniques to improve the quality of requirements are thought worth of repaying some research efforts, so the issue has been studied for years in the academic world and several solutions are proposed in literature. In this paper, a short survey of the existing solutions is presented and an approach that makes use of a model, a tool and a process to analyse the quality of requirements is proposed and compared. Then the results of applying the approach to the case study of requirements for train-control design, issued by the European Railway Agency, are reported and discussed. Also an industrial experience of a Service Centre about requirement analysis is shown and related application research issues are proposed.Source: 8th International Conference on the Quality of Information and Communications Technology, Lisboa, Portugal, 3-6 September 2012
Biscoglio I., Coco A., Fabbrini F., Fusani M., Lami G., Marchetti E., Trentanni G.
Requirements analysis occupies a prominent part in the activities of a product life cycle. Out of the various aspects of the analysis, those related to the quality of requirements can have a large impact in the quality of the final product. Since requirements are first conceived as natural language expressions, and intensive use of automation is advised to keep project cost at reasonable level, it seems opportune to develop requirements analysis by means of natural language processing techniques. In spite of the scarce interest drawn by these issues within the industrial environment, the advantages of adopting natural language processing techniques to improve the quality of requirements are thought worth of repaying some research efforts, so the issue has been studied for years in the academic world and several solutions are proposed in literature. In this paper, a short survey of the existing solutions is presented and an approach that makes use of a model, a tool and a process to analyse the quality of requirements is proposed and compared. Then the results of applying the approach to the case study of requirements for train-control design, issued by the European Railway Agency, are reported and discussed. Also an industrial experience of a Service Centre about requirement analysis is shown and related application research issues are proposed.Source: 8th International Conference on the Quality of Information and Communications Technology, Lisboa, Portugal, 3-6 September 2012
See at:
2012.quatic.org | CNR ExploRA
2011
Report
Open Access
QuARS versus QuARS Express
Trentanni G.
QuARS and QuARS Express (Quality Analyzer of Requirements Specifications) are tools that make it easier to extract structured information and metrics for detecting linguistic inaccuracies and defects in software requirements expressed in Natural language. The Express edition of QuARS represent a parallel evolution of the main tool exploiting the same core engine for an increased usability and a more expressive set of reports. In this article a comparison is presented.Source: ISTI Technical reports, 2011
Trentanni G.
QuARS and QuARS Express (Quality Analyzer of Requirements Specifications) are tools that make it easier to extract structured information and metrics for detecting linguistic inaccuracies and defects in software requirements expressed in Natural language. The Express edition of QuARS represent a parallel evolution of the main tool exploiting the same core engine for an increased usability and a more expressive set of reports. In this article a comparison is presented.Source: ISTI Technical reports, 2011
See at:
ISTI Repository | CNR ExploRA
2011
Report
Open Access
Addressing Readability in NL Requirements Analysis
Trentanni, G.
What is "readability" and why does it matter? According to Wikipedia (2006), "Readability is a measure of the accessibility of a piece of writing, indicating how wide an audience it will reach. Readability is a judgment of how easy a text is to understand". In the following the use of Readability Metrics in automated analysis of Natural Language expressed Requirements is investigated and some use case is presented.Source: ISTI Technical reports, 2011
Trentanni, G.
What is "readability" and why does it matter? According to Wikipedia (2006), "Readability is a measure of the accessibility of a piece of writing, indicating how wide an audience it will reach. Readability is a judgment of how easy a text is to understand". In the following the use of Readability Metrics in automated analysis of Natural Language expressed Requirements is investigated and some use case is presented.Source: ISTI Technical reports, 2011
See at:
ISTI Repository | CNR ExploRA
2011
Report
Open Access
The HAL-online Tool
Gnesi S., Trentanni G.
The HD-Automata Laboratory (HAL) is an integrated tool set for the specification, verification and analysis of concurrent and distributed systems. The core of HAL are the HD-automata: they are used as a common format for the various history-dependent languages. The HAL environment includes modules which implement decision procedures to calculate behavioral equivalences, and modules which support verification of behavioral properties expressed as formulae of suitable temporal logics. At this moment HAL works only with concurrent and distributed systems expressed by pi-calculus formalism. The HAL environment allows pi-calculus agents to be translated into ordinary automata, so that existing equivalence checkers can be used to calculate whether the pi-calculus are bisimilar. The environment also supports verification of logical formulae expressing desired properties of the behavior of pi-calculus agents. In this paper the online version of the toolkit is shown.Source: ISTI Technical reports, 2011
Gnesi S., Trentanni G.
The HD-Automata Laboratory (HAL) is an integrated tool set for the specification, verification and analysis of concurrent and distributed systems. The core of HAL are the HD-automata: they are used as a common format for the various history-dependent languages. The HAL environment includes modules which implement decision procedures to calculate behavioral equivalences, and modules which support verification of behavioral properties expressed as formulae of suitable temporal logics. At this moment HAL works only with concurrent and distributed systems expressed by pi-calculus formalism. The HAL environment allows pi-calculus agents to be translated into ordinary automata, so that existing equivalence checkers can be used to calculate whether the pi-calculus are bisimilar. The environment also supports verification of logical formulae expressing desired properties of the behavior of pi-calculus agents. In this paper the online version of the toolkit is shown.Source: ISTI Technical reports, 2011
See at:
ISTI Repository | CNR ExploRA